Termination of the given ITRSProblem could not be shown:



↳ ITRS
  ↳ ITRStoIDPProof

ITRS problem:
The following domains are used:

z

The TRS R consists of the following rules:

f91(n) → cond(<=@z(n, 100@z), n)
cond(TRUE, n) → f91(f91(+@z(n, 11@z)))
cond(FALSE, n) → -@z(n, 10@z)

The set Q consists of the following terms:

f91(x0)
cond(TRUE, x0)
cond(FALSE, x0)


Added dependency pairs

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ IDPtoQDPProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

f91(n) → cond(<=@z(n, 100@z), n)
cond(TRUE, n) → f91(f91(+@z(n, 11@z)))
cond(FALSE, n) → -@z(n, 10@z)

The integer pair graph contains the following rules and edges:

(0): COND(TRUE, n[0]) → F91(f91(+@z(n[0], 11@z)))
(1): F91(n[1]) → COND(<=@z(n[1], 100@z), n[1])
(2): COND(TRUE, n[2]) → F91(+@z(n[2], 11@z))

(0) -> (1), if ((f91(+@z(n[0], 11@z)) →* n[1]))


(1) -> (0), if ((n[1] →* n[0])∧(<=@z(n[1], 100@z) →* TRUE))


(1) -> (2), if ((n[1] →* n[2])∧(<=@z(n[1], 100@z) →* TRUE))


(2) -> (1), if ((+@z(n[2], 11@z) →* n[1]))



The set Q consists of the following terms:

f91(x0)
cond(TRUE, x0)
cond(FALSE, x0)


Represented integers and predefined function symbols by Terms

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ IDPtoQDPProof
        ↳ QDP
          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

COND(true, n[0]) → F91(f91(plus_int(pos(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), n[0])))
F91(n[1]) → COND(lesseq_int(n[1], pos(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), n[1])
COND(true, n[2]) → F91(plus_int(pos(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), n[2]))

The TRS R consists of the following rules:

f91(n) → cond(lesseq_int(n, pos(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), n)
cond(true, n) → f91(f91(plus_int(pos(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), n)))
cond(false, n) → minus_int(n, pos(s(s(s(s(s(s(s(s(s(s(0))))))))))))
lesseq_int(pos(0), pos(y)) → true
lesseq_int(pos(0), neg(0)) → true
lesseq_int(neg(x), pos(y)) → true
lesseq_int(neg(x), neg(0)) → true
lesseq_int(pos(x), neg(s(y))) → false
lesseq_int(neg(0), neg(s(y))) → false
lesseq_int(pos(s(x)), pos(0)) → false
lesseq_int(pos(s(x)), neg(y)) → false
lesseq_int(pos(s(x)), pos(s(y))) → lesseq_int(pos(x), pos(y))
lesseq_int(neg(s(x)), neg(s(y))) → lesseq_int(neg(x), neg(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), neg(y)) → minus_nat(y, x)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
minus_int(pos(x), neg(y)) → pos(plus_nat(x, y))

The set Q consists of the following terms:

f91(x0)
cond(true, x0)
cond(false, x0)
lesseq_int(pos(0), pos(x0))
lesseq_int(pos(0), neg(0))
lesseq_int(neg(x0), pos(x1))
lesseq_int(neg(x0), neg(0))
lesseq_int(pos(x0), neg(s(x1)))
lesseq_int(neg(0), neg(s(x0)))
lesseq_int(pos(s(x0)), pos(0))
lesseq_int(pos(s(x0)), neg(x1))
lesseq_int(pos(s(x0)), pos(s(x1)))
lesseq_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ IDPtoQDPProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

COND(true, n[0]) → F91(f91(plus_int(pos(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), n[0])))
F91(n[1]) → COND(lesseq_int(n[1], pos(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), n[1])
COND(true, n[2]) → F91(plus_int(pos(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), n[2]))

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
cond(true, n) → f91(f91(plus_int(pos(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), n)))
f91(n) → cond(lesseq_int(n, pos(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), n)
lesseq_int(pos(0), pos(y)) → true
lesseq_int(neg(x), pos(y)) → true
lesseq_int(pos(s(x)), pos(s(y))) → lesseq_int(pos(x), pos(y))
cond(false, n) → minus_int(n, pos(s(s(s(s(s(s(s(s(s(s(0))))))))))))
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
lesseq_int(pos(s(x)), pos(0)) → false

The set Q consists of the following terms:

f91(x0)
cond(true, x0)
cond(false, x0)
lesseq_int(pos(0), pos(x0))
lesseq_int(pos(0), neg(0))
lesseq_int(neg(x0), pos(x1))
lesseq_int(neg(x0), neg(0))
lesseq_int(pos(x0), neg(s(x1)))
lesseq_int(neg(0), neg(s(x0)))
lesseq_int(pos(s(x0)), pos(0))
lesseq_int(pos(s(x0)), neg(x1))
lesseq_int(pos(s(x0)), pos(s(x1)))
lesseq_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule COND(true, n[0]) → F91(f91(plus_int(pos(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), n[0]))) at position [0] we obtained the following new rules [LPAR04]:

COND(true, n[0]) → F91(cond(lesseq_int(plus_int(pos(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), n[0]), pos(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), plus_int(pos(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), n[0])))



↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ IDPtoQDPProof
        ↳ QDP
          ↳ UsableRulesProof
            ↳ QDP
              ↳ Rewriting
                ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

F91(n[1]) → COND(lesseq_int(n[1], pos(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), n[1])
COND(true, n[2]) → F91(plus_int(pos(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), n[2]))
COND(true, n[0]) → F91(cond(lesseq_int(plus_int(pos(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), n[0]), pos(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), plus_int(pos(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), n[0])))

The TRS R consists of the following rules:

plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
cond(true, n) → f91(f91(plus_int(pos(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))), n)))
f91(n) → cond(lesseq_int(n, pos(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), n)
lesseq_int(pos(0), pos(y)) → true
lesseq_int(neg(x), pos(y)) → true
lesseq_int(pos(s(x)), pos(s(y))) → lesseq_int(pos(x), pos(y))
cond(false, n) → minus_int(n, pos(s(s(s(s(s(s(s(s(s(s(0))))))))))))
minus_int(pos(x), pos(y)) → minus_nat(x, y)
minus_int(neg(x), pos(y)) → neg(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
lesseq_int(pos(s(x)), pos(0)) → false

The set Q consists of the following terms:

f91(x0)
cond(true, x0)
cond(false, x0)
lesseq_int(pos(0), pos(x0))
lesseq_int(pos(0), neg(0))
lesseq_int(neg(x0), pos(x1))
lesseq_int(neg(x0), neg(0))
lesseq_int(pos(x0), neg(s(x1)))
lesseq_int(neg(0), neg(s(x0)))
lesseq_int(pos(s(x0)), pos(0))
lesseq_int(pos(s(x0)), neg(x1))
lesseq_int(pos(s(x0)), pos(s(x1)))
lesseq_int(neg(s(x0)), neg(s(x1)))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
minus_int(pos(x0), pos(x1))
minus_int(neg(x0), neg(x1))
minus_int(neg(x0), pos(x1))
minus_int(pos(x0), neg(x1))

We have to consider all minimal (P,Q,R)-chains.